Inference at * 1 1 2 
Iof proof for Lemma l before antisymmetry:



1. T : Type
2. l : T List
3. x : T
4. y : T
5. no_repeats(T;l)
6. [x; y]  l
7. [y; x]  l
  [x; y; x]  l 

latex

 by InteriorProof ((((((InstLemma `append_overlapping_sublists`  
[T;[x];[x];l;y]) 
[CollapseTHEN (
[CollapseTHEN ((Auto_aux (first_nat 1:n) ((first_nat 1:n),(first_nat 3:n)) (first_tok :t
[CollapseTHEN () inil_term)))) 
[CollapseTHEN (All Reduce))) 
[CollapseTHEN (
[CollapseTHEN ((Auto_aux (first_nat 1:n) ((first_nat 1:n),(first_nat 4:n)) (first_tok :t
[CollapseTHEN () inil_term))) 

latex

[C.

Definitions	Y, as @ bs, t  T, P  Q, x:A. B(x)
Lemmas	append overlapping sublists